// Copyright 2007-2009, Stanford University. All Rights Reserved.
// Copyright 2010-2011, Dependable Systems Lab, EPFL. All Rights Reserved.
// Copyright 2012, Google Inc. All Rights Reserved.
//
// Redistribution and use in source and binary forms, with or without
// modification, are permitted provided that the following conditions are
// met:
//
//     * Redistributions of source code must retain the above copyright
// notice, this list of conditions and the following disclaimers.
//     * Redistributions in binary form must reproduce the above
// copyright notice, this list of conditions and the following disclaimers
// in the documentation and/or other materials provided with the
// distribution.
//     * Neither the names of the klee Team, Stanford University, nor the
// names of its contributors may be used to endorse or promote
// products derived from the software without specific prior
// written permission. Neither the names of the Dependable Systems
// Laboratory, EPFL, nor the names of its contributors may be used to
// endorse or promote products derived from the software without prior
// written permission. Neither the names of Google Inc. nor the names of
// its contributors may be used to endorse or promote products derived from
// the software without specific prior written permission.
//
// THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
// "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
// LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
// A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
// OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
// SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
// LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
// DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
// THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
// (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
// OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.

#ifndef SRC_SOLVER_SOLVER_H_
#define SRC_SOLVER_SOLVER_H_

#include "expr/Expr.h"
#include "util/Ref.h"

#include <vector>

namespace seven_summits {
namespace expr {
class ConstraintManager;  // "expr/Constraints.h"
}
}
namespace seven_summits {
namespace solver {

using expr::Array;
using expr::ConstraintManager;
using expr::ConstantExpr;
using expr::Expr;
using util::ref;

class SolverImpl;         // "solver/SolverImpl.h"

struct Query {
public:
  const ConstraintManager &constraints;
  ref<Expr> expr;

  Query(const ConstraintManager& _constraints, ref<Expr> _expr)
    : constraints(_constraints), expr(_expr) {
  }

  /// withExpr - Return a copy of the query with the given expression.
  Query withExpr(ref<Expr> _expr) const {
    return Query(constraints, _expr);
  }

  /// withFalse - Return a copy of the query with a false expression.
  Query withFalse() const {
    return Query(constraints, ConstantExpr::alloc(0, Expr::Bool));
  }

  /// negateExpr - Return a copy of the query with the expression negated.
  Query negateExpr() const {
    return withExpr(Expr::createIsZero(expr));
  }
};

class Solver {
public:
  enum Validity {
    True = 1,
    False = -1,
    Unknown = 0
  };

  /// validity_to_str - Return the name of given Validity enum value.
  static const char *validity_to_str(Validity v);

  SolverImpl *impl;  // TODO(bqe): Does this have to be public?

  Solver(SolverImpl *_impl) : impl(_impl) {}
  virtual ~Solver();

  /// evaluate - Determine the full validity of an expression in particular
  /// state.
  ////
  /// \param [out] result - The validity of the given expression (provably
  /// true, provably false, or neither).
  ///
  /// \return True on success.
  bool evaluate(const Query&, Validity &result);

  /// mustBeTrue - Determine if the expression is provably true.
  ///
  /// \param [out] result - On success, true iff the expresssion is provably
  /// false.
  ///
  /// \return True on success.
  bool mustBeTrue(const Query&, bool &result);

  /// mustBeFalse - Determine if the expression is provably false.
  ///
  /// \param [out] result - On success, true iff the expresssion is provably
  /// false.
  ///
  /// \return True on success.
  bool mustBeFalse(const Query&, bool &result);

  /// mayBeTrue - Determine if there is a valid assignment for the given state
  /// in which the expression evaluates to false.
  ///
  /// \param [out] result - On success, true iff the expresssion is true for
  /// some satisfying assignment.
  ///
  /// \return True on success.
  bool mayBeTrue(const Query&, bool &result);

  /// mayBeFalse - Determine if there is a valid assignment for the given
  /// state in which the expression evaluates to false.
  ///
  /// \param [out] result - On success, true iff the expresssion is false for
  /// some satisfying assignment.
  ///
  /// \return True on success.
  bool mayBeFalse(const Query&, bool &result);

  /// getValue - Compute one possible value for the given expression.
  ///
  /// \param [out] result - On success, a value for the expression in some
  /// satisying assignment.
  ///
  /// \return True on success.
  bool getValue(const Query&, ref<ConstantExpr> &result);

  /// getInitialValues - Compute the initial values for a list of objects.
  ///
  /// \param [out] result - On success, this vector will be filled in with an
  /// array of bytes for each given object (with length matching the object
  /// size). The bytes correspond to the initial values for the objects for
  /// some satisying assignment.
  ///
  /// \return True on success.
  ///
  /// NOTE: This function returns failure if there is no satisfying
  /// assignment.
  //
  // FIXME: This API is lame. We should probably just provide an API which
  // returns an Assignment object, then clients can get out whatever values
  // they want. This also allows us to optimize the representation.
  bool getInitialValues(const Query&,
                        const std::vector<const Array*> &objects,
                        std::vector< std::vector<unsigned char> > &result);

  /// getRange - Compute a tight range of possible values for a given
  /// expression.
  ///
  /// \return - A pair with (min, max) values for the expression.
  ///
  /// \post(mustBeTrue(min <= e <= max) &&
  ///       mayBeTrue(min == e) &&
  ///       mayBeTrue(max == e))
  //
  // FIXME: This should go into a helper class, and should handle failure.
  virtual std::pair< ref<Expr>, ref<Expr> > getRange(const Query&);

private:
  // DO NOT IMPLEMENT.
  Solver(const Solver&);
  void operator=(const Solver&);
};

/// STPSolver - A complete solver based on STP.
class STPSolver : public Solver {
public:
  /// STPSolver - Construct a new STPSolver.
  ///
  /// \param optimizeDivides - Whether constant division operations should
  /// be optimized into add/shift/multiply operations.
  STPSolver(bool optimizeDivides = true);

  /// getConstraintLog - Return the constraint log for the given state in CVC
  /// format.
  char *getConstraintLog(const Query&);

  /// setTimeout - Set constraint solver timeout delay to the given value; 0
  /// is off.
  void setTimeout(double timeout);
};

/* *** */

/// createValidatingSolver - Create a solver which will validate all query
/// results against an oracle, used for testing that an optimized solver has
/// the same results as an unoptimized one. This solver will assert on any
/// mismatches.
///
/// \param s - The primary underlying solver to use.
/// \param oracle - The solver to check query results against.
Solver *createValidatingSolver(Solver *s, Solver *oracle);

/// createCachingSolver - Create a solver which will cache the queries in
/// memory (without eviction).
///
/// \param s - The underlying solver to use.
Solver *createCachingSolver(Solver *s);

/// createCexCachingSolver - Create a counterexample caching solver. This is a
/// more sophisticated cache which records counterexamples for a constraint
/// set and uses subset/superset relations among constraints to try and
/// quickly find satisfying assignments.
///
/// \param s - The underlying solver to use.
Solver *createCexCachingSolver(Solver *s);

/// createFastCexSolver - Create a "fast counterexample solver", which tries
/// to quickly compute a satisfying assignment for a constraint set using
/// value propogation and range analysis.
///
/// \param s - The underlying solver to use.
Solver *createFastCexSolver(Solver *s);

/// createIndependentSolver - Create a solver which will eliminate any
/// unnecessary constraints before propogating the query to the underlying
/// solver.
///
/// \param s - The underlying solver to use.
Solver *createIndependentSolver(Solver *s);

/// createPCLoggingSolver - Create a solver which will forward all queries
/// after writing them to the given path in .pc format.
Solver *createPCLoggingSolver(Solver *s, std::string path);

/// createDummySolver - Create a dummy solver implementation which always
/// fails.
Solver *createDummySolver();
}  // namespace expr
}  // namespace seven_summits

#endif  // SRC_SOLVER_SOLVER_H_
